Nuprl Lemma : EState-subtype-EOrder
11,40
postcript
pdf
EventsWithState
r EventsWithOrder
latex
Definitions
Top
,
t
T
,
Void
,
x
:
A
.
B
(
x
)
,
<
a
,
b
>
,
x
:
A
B
(
x
)
,
Type
,
x
:
A
.
B
(
x
)
,
EOrderAxioms(
E
;
pred?
;
info
)
,
Id
,
x
:
A
B
(
x
)
,
S
T
,
IdLnk
,
left
+
right
,
f
(
a
)
,
Unit
,
EqDecider(
T
)
,
EventsWithState
,
EventsWithOrder
Lemmas
E-State
wf
,
EOrder
wf
,
deq
wf
,
unit
wf
,
IdLnk
wf
,
Id
wf
,
EOrderAxioms
wf
,
top
wf
origin
T, Void, 
x:A.B(x), <a, b>, x:A 
B(x), Type, 
x:A. B(x), EOrderAxioms(E; pred?; info), Id, x:A
B(x), S 
T, IdLnk, left + right, f(a), Unit, EqDecider(T), EventsWithState, EventsWithOrder